package formula;

import atom.Atom;
import atom.UnaryAtom;
import literal.UnaryLiteral;
import sign.FormulaSign;
import java.util.Objects;

public class BinaryFormula extends Formula{
    FormulaSign sign;
    Formula left;
    Formula right;

    public BinaryFormula(FormulaSign sign,Formula left,Formula right){
        this.sign=sign;
        this.left=left;
        this.right=right;
    }

    @Override
    public String toString(){
        return sign + "(" + left + "," + right + ")";
    }

    public FormulaSign getSign(){
        return sign;
    }
    public Formula getLeft(){
        return left;
    }
    public Formula getRight(){
        return right;
    }

    @Override
    public boolean equals(Object o) {
        if (this == o) return true;
        if (o instanceof StarFormula){return true;}
        if (o == null || getClass() != o.getClass()) return false;
        BinaryFormula that = (BinaryFormula) o;
        //return toString().equals(that.toString());
        return sign == that.sign && Objects.equals(left, that.left) && Objects.equals(right, that.right);
    }

    @Override
    public int hashCode() {
        return Objects.hash(sign, left, right);
    }

//    public FormulaSign getSign(BinaryFormula f1){
//        return f1.sign;
//    }

    @Override
    public BinaryFormula getNegated() {
        // TODO: implement this
        //System.out.println("old formula is: " + this.toString());
        if (this.sign.equals(FormulaSign.ANY)) {//sign==ANY,return new formula with EXIST
            //not ANY(p,q) = EXIST(p,not q)
            FormulaSign sign = FormulaSign.EXIST;
            if (this.getRight() instanceof UnaryFormula){//正常bf情况，右侧是uf
                UnaryFormula right_formula = (UnaryFormula) this.getRight();
                Atom right_atom = right_formula.literal.getAtom();
                boolean atom_negated=right_formula.literal.getNegated();//获取这个元素是否带“not”符号
                if (atom_negated){//true,该元素带“not”符号，新的formula不带“not”符号
                    UnaryFormula new_f=new UnaryFormula(new UnaryLiteral(right_atom,false));
                    return new BinaryFormula(FormulaSign.EXIST,this.getLeft(),new_f);
                }else {//false,该元素不带“not”符号，新的formula带“not”符号
                    UnaryFormula new_f=new UnaryFormula(new UnaryLiteral(right_atom,true));
                    return new BinaryFormula(FormulaSign.EXIST,this.getLeft(),new_f);
                }
            }else{//此时为tf，右侧为bf
                BinaryFormula bfR=(BinaryFormula) this.getRight();
                FormulaSign signR=bfR.sign;
                if (signR.equals(FormulaSign.ANY)){//两种情况分析。此时为AA情况
                    //ANY(p,ANY(q,t))->EXIST(p,EXIST(q,not t))
                    UnaryFormula ufR=(UnaryFormula) bfR.getRight();//t
                    UnaryFormula ufRN=ufR.getNegated();//not t
                    BinaryFormula bfRN=new BinaryFormula(FormulaSign.EXIST,bfR.getLeft(),ufRN);
                    BinaryFormula result=new BinaryFormula(FormulaSign.EXIST,this.getLeft(),bfRN);
                    return result;
                }else {//AE
                    //ANY(p,EXIST(q,t))->EXIST(p,ANY(q,not t))
                    UnaryFormula ufR=(UnaryFormula) bfR.getRight();//t
                    UnaryFormula ufRN=ufR.getNegated();//not t
                    BinaryFormula bfRN=new BinaryFormula(FormulaSign.ANY,bfR.getLeft(),ufRN);
                    BinaryFormula result=new BinaryFormula(FormulaSign.EXIST,this.getLeft(),bfRN);
                    return result;
                }
            }

        } else {//sign==EXIST,return new formula with ANY
            FormulaSign sign = FormulaSign.ANY;
            // not ∃(beekeeper, hate) = ∀(beekeeper, not hate),(对EXIST取反的例子)
            // not EXIST(p,q) = ANY(p,not q)
            //this.left=this.getLeft();//左侧不改变
            if (this.getRight() instanceof UnaryFormula){//正常bf，右侧为uf
                UnaryFormula right_formula = (UnaryFormula) this.getRight();
                Atom right_atom = right_formula.literal.getAtom();
                boolean atom_negated=right_formula.literal.getNegated();//获取这个元素是否带“not”符号
                if (atom_negated){//true,该元素带“not”符号，新的formula不带“not”符号
                    UnaryFormula new_f=new UnaryFormula(new UnaryLiteral(right_atom,false));
                    return new BinaryFormula(FormulaSign.ANY,this.getLeft(),new_f);
                }else {//false,该元素不带“not”符号，新的formula带“not”符号
                    UnaryFormula new_f=new UnaryFormula(new UnaryLiteral(right_atom,true));
                    return new BinaryFormula(FormulaSign.ANY,this.getLeft(),new_f);
                }
            }else {//此时为tf，右侧为bf
                BinaryFormula bfR=(BinaryFormula) this.getRight();
                FormulaSign signR=bfR.sign;
                if (signR.equals(FormulaSign.ANY)){//两种情况分析。此时为EA情况，注意，EA没有在规则中被应用过
                    //EXIST(p,ANY(q,t))->ANY(p,EXIST(q,not t))
                    UnaryFormula ufR=(UnaryFormula) bfR.getRight();//t
                    UnaryFormula ufRN=ufR.getNegated();//not t
                    BinaryFormula bfRN=new BinaryFormula(FormulaSign.EXIST,bfR.getLeft(),ufRN);
                    BinaryFormula result=new BinaryFormula(FormulaSign.ANY,this.getLeft(),bfRN);
                    return result;
                }else {//EE
                    //EXIST(p,EXIST(q,t))->ANY(p,ANY(q,not t))
                    UnaryFormula ufR=(UnaryFormula) bfR.getRight();//t
                    UnaryFormula ufRN=ufR.getNegated();//not t
                    BinaryFormula bfRN=new BinaryFormula(FormulaSign.ANY,bfR.getLeft(),ufRN);
                    BinaryFormula result=new BinaryFormula(FormulaSign.ANY,this.getLeft(),bfRN);
                    return result;
                }
            }

        }
    }

    @Override
    public boolean isNegated(Formula f) {
        if (f instanceof BinaryFormula){
            BinaryFormula f2=(BinaryFormula) f;
            BinaryFormula tmp_bf=this.getNegated();
            if (tmp_bf.equals(f2)){//二者互斥
                return true;
            }else {
                return false;
            }
        }else if (f instanceof StarFormula){
            return true;
        }
        return false;
    }


}
